; COMMAND-LINE: --lfsc-flatten --lfsc-expand-trust
; EXPECT: unsat

(set-logic QF_UFLIRA)
(declare-sort FArray 2)


;-------------------------------------------------------------------------------
; Constants :
;-------------------------------------------------------------------------------



;-------------------------------------------------------------------------------
; State variables :
;-------------------------------------------------------------------------------

(declare-fun add_two.usr.a (Int) Real)
(declare-fun add_two.usr.b (Int) Real)
(declare-fun add_two.usr.c (Int) Real)
(declare-fun add_two.res.init_flag (Int) Bool)
(declare-fun add_two.impl.usr.P (Int) Bool)
(set-info :system "Logical transition system generated by Kind2")
(set-info :input "add_two.lus")



;-------------------------------------------------------------------------------
; Function symbols :
;-------------------------------------------------------------------------------

(define-fun __node_init_add_two_0
 ((add_two.usr.a@0 Real)
  (add_two.usr.b@0 Real)
  (add_two.usr.c@0 Real)
  (add_two.res.init_flag@0 Bool)
  (add_two.impl.usr.P@0 Bool)) Bool
 (let
  ((X1 (+ add_two.usr.a@0 add_two.usr.b@0)))
  (and
   (= add_two.usr.c@0 1.0)
   (= add_two.impl.usr.P@0 (=> (and (> add_two.usr.a@0 0.0) (> add_two.usr.b@0 0.0)) (> add_two.usr.c@0 0.0)))
   add_two.res.init_flag@0)))

(define-fun __node_trans_add_two_0
 ((add_two.usr.a@1 Real)
  (add_two.usr.b@1 Real)
  (add_two.usr.c@1 Real)
  (add_two.res.init_flag@1 Bool)
  (add_two.impl.usr.P@1 Bool)
  (add_two.usr.a@0 Real)
  (add_two.usr.b@0 Real)
  (add_two.usr.c@0 Real)
  (add_two.res.init_flag@0 Bool)
  (add_two.impl.usr.P@0 Bool)) Bool
 (let
  ((X1 (+ add_two.usr.a@1 add_two.usr.b@1)))
  (and
   (= add_two.usr.c@1 (ite (> add_two.usr.c@0 X1) add_two.usr.c@0 X1))
   (= add_two.impl.usr.P@1 (=> (and (> add_two.usr.a@1 0.0) (> add_two.usr.b@1 0.0)) (> add_two.usr.c@1 0.0)))
   (not add_two.res.init_flag@1))))



;-------------------------------------------------------------------------------
; Initial states :
;-------------------------------------------------------------------------------

(define-fun I1 ((i Int)) Bool
 (__node_init_add_two_0
  (add_two.usr.a i)
  (add_two.usr.b i)
  (add_two.usr.c i)
  (add_two.res.init_flag i)
  (add_two.impl.usr.P i)))



;-------------------------------------------------------------------------------
; Transition_relation :
;-------------------------------------------------------------------------------

(define-fun T1 ((i Int) (j Int)) Bool
 (__node_trans_add_two_0
  (add_two.usr.a j)
  (add_two.usr.b j)
  (add_two.usr.c j)
  (add_two.res.init_flag j)
  (add_two.impl.usr.P j)
  (add_two.usr.a i)
  (add_two.usr.b i)
  (add_two.usr.c i)
  (add_two.res.init_flag i)
  (add_two.impl.usr.P i)))



;-------------------------------------------------------------------------------
; Original property :
;-------------------------------------------------------------------------------

(define-fun P1 ((i Int)) Bool (add_two.impl.usr.P i))



;-------------------------------------------------------------------------------
; k-Inductive invariant :
;-------------------------------------------------------------------------------

(define-fun PHI1 ((i Int)) Bool (add_two.impl.usr.P i))



;-------------------------------------------------------------------------------
; Base case :
;-------------------------------------------------------------------------------

(assert (and (I1 0) (not (PHI1 0))))

(check-sat)
(exit)
